FDL - Nuprl Definition : sum_of

Nuprl Definition : sum_of_torder

11,40

sum_of_torder(T;R)
==

a, b, x:T. ((R(a,x) & R(b,x))

(R(x,a) & R(x,b)))

(((R(a,b))

(a = b))

(R(b,a)))

clarification:

sum_of_torder(T;R)
==

a:T.
==

b:T, x:T. ((R(a,x) & R(b,x))

(R(x,a) & R(x,b)))

(((R(a,b))

(a = b

T))

(R(b,a)))

Definitions x:A. B(x), P Q, P & Q, P Q, s = t, f(a)

FDL editor aliases sum_of_torder

Definitions	x:A. B(x), P Q, P & Q, P Q, s = t, f(a)
FDL editor aliases	sum_of_torder